$i$ $<$z $j$ $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$if $i$$<$$j$ then tt else ff